$\forall$$A$,$B$:Type. b{-}union($A$; $B$) $\in$ Type